T:Type, L1, L2, L3:(T List). L1  L2  L3 || L2  L3 || L1 

latex

Definitions	t  T, P  Q, P & Q, P  Q, x:A. B(x), l1 || l2, l1  l2
Lemmas	compat wf, iseg wf, compat-iseg, compat symmetry